﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;
using HeapSpecSupport;
using SimpleIR;

namespace Evaluator.EvalState
{
	/// <summary>
	/// This class is used to represent the special array class object values.
	/// </summary>
	internal sealed class EArrayObject : EBuiltinObject
	{
		internal readonly IRMemberField CardField;
		internal readonly IRMemberField ContentsField;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.CardField != null);
			Contract.Invariant(this.ContentsField != null);
		}

		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and <c>acontents</c> array.
		/// </summary>
		private EArrayObject(int address, IRContainerType tt, AllocRecord alloc, BAPLayoutMap fvalues, IRMemberField cardf, IRMemberField contentsf)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(cardf != null);
			Contract.Requires(contentsf != null);
			
			this.CardField = cardf;
			this.ContentsField = contentsf;
		}

		/// <summary>
		/// Allocate and set all the fields to the needed values for an array type value.
		/// </summary>
		internal static EArrayObject CreateFreshArrayValueForType(int address, IRContainerType tt, int length, ulong time, long line)
		{
			Contract.Requires(tt != null && tt.IsArrayContainer);
			Contract.Ensures(Contract.Result<EArrayObject>() != null);

			IRMemberField cardf = tt.TypeDescription.GetFieldWithNameDefIn("card");
			IRMemberField contf = tt.TypeDescription.GetFieldWithNameDefIn("allf");

			HashSet<IRBasicAccessPath> cntspths = new HashSet<IRBasicAccessPath>();
			if(tt.ContainerContentsType is IRStructType)
			{
				IRBasicAccessPath cpath = ExeProgram.TProg.GetAccessPathForSingleField(contf);
				foreach(IRBasicAccessPath ebap in tt.ContainerContentsType.TypeDescription.AllTerminalAccessPaths)
					cntspths.Add(ExeProgram.TProg.GetAccessPathExtensionPost_WPath(cpath, ebap));
			}
			else
			{
				IRBasicAccessPath cpath = ExeProgram.TProg.GetAccessPathForSingleField(contf);
				cntspths.Add(cpath);
			}

			BAPLayoutMap fve = new BAPLayoutMap(length, cntspths, tt.TypeDescription.AllTerminalAccessPaths, time, line);
			AllocRecord alloc = new AllocRecord(time, line);

			EArrayObject aao = new EArrayObject(address, tt, alloc, fve, cardf, contf);
			aao.SimulateObjectConstructor(time, line);

			ENumeric plength = new ENumeric((IRSignedIntegerType)cardf.FieldType, length);
			IRBasicAccessPath lenp = ExeProgram.TProg.GetAccessPathForSingleField(cardf);
			aao.DoSimpleValueWriteToLocation(BAPLayoutEntry.INVALID_ARRAY_INDEX, lenp, plength, time, line);

			return aao;
		}

		public override string ToString()
		{
			StringBuilder sb = new StringBuilder("[" + this.m_loctype.ToString() + ": ");
			sb.Append(this.m_fieldinfo.ToString());
			sb.Append("]");

			return sb.ToString();
		}

		internal override EValue DoSimpleValueReadFromLocation(int arrayidx, IRBasicAccessPath bap, ulong time, long line)
		{
			Contract.Assert(arrayidx != BAPLayoutEntry.INVALID_ARRAY_INDEX);
			Contract.Assert(bap != null);

			return this.m_fieldinfo.ReadFieldValue(arrayidx, bap, time, line);
		}

		internal override void DoSimpleValueWriteToLocation(int arrayidx, IRBasicAccessPath bap, EValue val, ulong time, long line)
		{
			Contract.Assert(arrayidx != BAPLayoutEntry.INVALID_ARRAY_INDEX);
			Contract.Assert(bap != null);

			this.m_fieldinfo.WriteFieldValue(arrayidx, bap, (EMemoryValue)val, time, line);
		}

		internal override void DoCompoundReadFromLocation(int arrayidx, IRBasicAccessPath bap, BAPLayoutMap into, ulong time, long line)
		{
			Contract.Assert(arrayidx != BAPLayoutEntry.INVALID_ARRAY_INDEX);
			Contract.Assert(bap != null);

			this.m_fieldinfo.ReadFieldValues(arrayidx, bap, into, time, line);
		}

		internal override void DoCompoundWriteToLocation(int arrayidx, IRBasicAccessPath bap, BAPLayoutMap from, ulong time, long line)
		{
			Contract.Assert(arrayidx != BAPLayoutEntry.INVALID_ARRAY_INDEX);
			Contract.Assert(bap != null);

			this.m_fieldinfo.WriteFieldValues(arrayidx, from, bap, time, line);
		}
	}

	/// <summary>
	/// This class is used to represent the special List(T) class object values.
	/// </summary>
	internal sealed class EListObject : EBuiltinObject
	{
		internal readonly IRMemberField CardField;
		internal readonly IRMemberField ContentsField;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.CardField != null);
			Contract.Invariant(this.ContentsField != null);
		}

		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and the list.
		/// </summary>
		private EListObject(int address, IRContainerType tt, AllocRecord alloc, BAPLayoutMap fvalues, IRMemberField cardf, IRMemberField allf)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(cardf != null);
			Contract.Requires(allf != null);
					
			this.CardField = cardf;
			this.ContentsField = allf;
		}

		/// <summary>
		/// Allocate and set all the fields to the default values for a list type value.
		/// </summary>
		internal static EListObject CreateFreshListValueForType(int address, IRContainerType tt, ulong time, long line)
		{
			Contract.Requires(tt != null);
			Contract.Ensures(Contract.Result<EListObject>() != null);

			IRMemberField cardf = tt.TypeDescription.GetFieldWithNameDefIn("card");
			IRMemberField contf = tt.TypeDescription.GetFieldWithNameDefIn("allf");

			HashSet<IRBasicAccessPath> cntspths = new HashSet<IRBasicAccessPath>();
			if(tt.ContainerContentsType is IRStructType)
			{
				IRBasicAccessPath cpath = ExeProgram.TProg.GetAccessPathForSingleField(contf);
				foreach(IRBasicAccessPath ebap in tt.ContainerContentsType.TypeDescription.AllTerminalAccessPaths)
					cntspths.Add(ExeProgram.TProg.GetAccessPathExtensionPost_WPath(cpath, ebap));
			}
			else
			{
				IRBasicAccessPath cpath = ExeProgram.TProg.GetAccessPathForSingleField(contf);
				cntspths.Add(cpath);
			}

			BAPLayoutMap fve = new BAPLayoutMap(4, cntspths, tt.TypeDescription.AllTerminalAccessPaths, time, line);
			AllocRecord alloc = new AllocRecord(time, line);

			EListObject elo = new EListObject(address, tt, alloc, fve, cardf, contf);
			elo.SimulateObjectConstructor(time, line);

			ENumeric plength = new ENumeric((IRSignedIntegerType)cardf.FieldType, 0);
			IRBasicAccessPath lenp = ExeProgram.TProg.GetAccessPathForSingleField(cardf);
			elo.DoSimpleValueWriteToLocation(BAPLayoutEntry.INVALID_ARRAY_INDEX, lenp, plength, time, line);

			return elo;
		}

		public override string ToString()
		{
			StringBuilder sb = new StringBuilder("[" + this.m_loctype.ToString() + ": ");
			sb.Append(this.m_fieldinfo.ToString());
			sb.Append("]");

			return sb.ToString();
		}
	}

	/// <summary>
	/// This class is used to represent the special HashSet(T) class object values.
	/// </summary>
	internal sealed class EHashSetObject : EBuiltinObject
	{
		internal const int INIT_CAPACITY = 8;

		internal readonly IRMemberField CardField;
		internal readonly IRMemberField CapacityField;
		internal readonly IRMemberField ContentsHashField;
		internal readonly IRMemberField ContentsField;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.CardField != null);
			Contract.Invariant(this.CapacityField != null);
			Contract.Invariant(this.ContentsHashField != null);
			Contract.Invariant(this.ContentsField != null);
		}

		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and the list.
		/// </summary>
		private EHashSetObject(int address, IRContainerType tt, AllocRecord alloc, BAPLayoutMap fvalues, IRMemberField cardf, IRMemberField capacityf, IRMemberField hashf, IRMemberField contentsf)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(tt != null);
			Contract.Requires(fvalues != null);
			Contract.Requires(cardf != null);
			Contract.Requires(capacityf != null);
			Contract.Requires(hashf != null);
			Contract.Requires(contentsf != null);
			
			this.CardField = cardf;
			this.CapacityField = capacityf;
			this.ContentsHashField = hashf;
			this.ContentsField = contentsf;
		}

		/// <summary>
		/// Allocate and set all the fields to the default values for a list type value.
		/// </summary>
		internal static EHashSetObject CreateFreshHashSetValueForType(int address, IRContainerType tt, ulong time, long line)
		{
			Contract.Requires(tt != null);
			Contract.Ensures(Contract.Result<EHashSetObject>() != null);

			IRMemberField cardf = tt.TypeDescription.GetFieldWithNameDefIn("card");
			IRMemberField capf = tt.TypeDescription.GetFieldWithNameDefIn("capacity");
			IRMemberField allh = tt.TypeDescription.GetFieldWithNameDefIn("allh");
			IRMemberField allf = tt.TypeDescription.GetFieldWithNameDefIn("allf");

			HashSet<IRBasicAccessPath> cntspths = new HashSet<IRBasicAccessPath>();
			if(tt.ContainerContentsType is IRStructType)
			{
				IRBasicAccessPath hpath = ExeProgram.TProg.GetAccessPathForSingleField(allh);
				IRBasicAccessPath fpath = ExeProgram.TProg.GetAccessPathForSingleField(allf);
				foreach(IRBasicAccessPath ebap in tt.ContainerContentsType.TypeDescription.AllTerminalAccessPaths)
				{
					cntspths.Add(ExeProgram.TProg.GetAccessPathExtensionPost_WPath(hpath, ebap));
					cntspths.Add(ExeProgram.TProg.GetAccessPathExtensionPost_WPath(fpath, ebap));
				}
			}
			else
			{
				IRBasicAccessPath hpath = ExeProgram.TProg.GetAccessPathForSingleField(allh);
				IRBasicAccessPath fpath = ExeProgram.TProg.GetAccessPathForSingleField(allf);
				cntspths.Add(hpath);
				cntspths.Add(fpath);
			}

			BAPLayoutMap fve = new BAPLayoutMap(INIT_CAPACITY, cntspths, tt.TypeDescription.AllTerminalAccessPaths, time, line);
			AllocRecord alloc = new AllocRecord(time, line);

			EHashSetObject hso = new EHashSetObject(address, tt, alloc, fve, cardf, capf, allf, allh);
			hso.SimulateObjectConstructor(time, line);

			ENumeric pcard = new ENumeric((IRSignedIntegerType)cardf.FieldType, 0);
			IRBasicAccessPath cardp = ExeProgram.TProg.GetAccessPathForSingleField(cardf);
			hso.DoSimpleValueWriteToLocation(BAPLayoutEntry.INVALID_ARRAY_INDEX, cardp, pcard, time, line);

			ENumeric pcap = new ENumeric((IRSignedIntegerType)cardf.FieldType, INIT_CAPACITY);
			IRBasicAccessPath capp = ExeProgram.TProg.GetAccessPathForSingleField(capf);
			hso.DoSimpleValueWriteToLocation(BAPLayoutEntry.INVALID_ARRAY_INDEX, capp, pcap, time, line);

			return hso;
		}

		public override string ToString()
		{
			StringBuilder sb = new StringBuilder("[" + this.m_loctype.ToString() + ": ");
			sb.Append(this.m_fieldinfo.ToString());
			sb.Append("]");

			return sb.ToString();
		}
	}

	/// <summary>
	/// This class is used to represent the special Dictionary(T) class object values.
	/// </summary>
	internal sealed class EDictionaryObject : EBuiltinObject
	{
		internal const int INIT_CAPACITY = 8;

		internal readonly IRMemberField CardField;
		internal readonly IRMemberField CapacityField;
		internal readonly IRMemberField ContentsHashField;
		internal readonly IRMemberField ContentsField;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.CardField != null);
			Contract.Invariant(this.CapacityField != null);
			Contract.Invariant(this.ContentsHashField != null);
			Contract.Invariant(this.ContentsField != null);
		}

		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and the list.
		/// </summary>
		private EDictionaryObject(int address, IRDictionaryType tt, AllocRecord alloc, BAPLayoutMap fvalues, IRMemberField cardf, IRMemberField capacityf, IRMemberField hashf, IRMemberField contentsf)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(tt != null);
			Contract.Requires(fvalues != null);
			Contract.Requires(cardf != null);
			Contract.Requires(capacityf != null);
			Contract.Requires(hashf != null);
			Contract.Requires(contentsf != null);

			this.CardField = cardf;
			this.CapacityField = capacityf;
			this.ContentsHashField = hashf;
			this.ContentsField = contentsf;
		}

		/// <summary>
		/// Allocate and set all the fields to the default values for a list type value.
		/// </summary>
		internal static EDictionaryObject CreateFreshDictionaryValue(int address, IRDictionaryType tt, ulong time, long line)
		{
			Contract.Requires(tt != null);
			Contract.Ensures(Contract.Result<EDictionaryObject>() != null);

			IRMemberField cardf = tt.TypeDescription.GetFieldWithNameDefIn("card");
			IRMemberField capf = tt.TypeDescription.GetFieldWithNameDefIn("capacity");
			IRMemberField allh = tt.TypeDescription.GetFieldWithNameDefIn("allh");
			IRMemberField allf = tt.TypeDescription.GetFieldWithNameDefIn("allf");

			HashSet<IRBasicAccessPath> cntspths = new HashSet<IRBasicAccessPath>();
			IRBasicAccessPath hpath = ExeProgram.TProg.GetAccessPathForSingleField(allh);
			IRBasicAccessPath fpath = ExeProgram.TProg.GetAccessPathForSingleField(allf);
			foreach(IRBasicAccessPath ebap in tt.ContainerContentsType.TypeDescription.AllTerminalAccessPaths)
			{
				cntspths.Add(ExeProgram.TProg.GetAccessPathExtensionPost_WPath(hpath, ebap));
				cntspths.Add(ExeProgram.TProg.GetAccessPathExtensionPost_WPath(fpath, ebap));
			}

			BAPLayoutMap fve = new BAPLayoutMap(INIT_CAPACITY, cntspths, tt.TypeDescription.AllTerminalAccessPaths, time, line);
			AllocRecord alloc = new AllocRecord(time, line);

			EDictionaryObject edo = new EDictionaryObject(address, tt, alloc, fve, cardf, capf, allf, allh);
			edo.SimulateObjectConstructor(time, line);

			ENumeric pcard = new ENumeric((IRSignedIntegerType)cardf.FieldType, 0);
			IRBasicAccessPath cardp = ExeProgram.TProg.GetAccessPathForSingleField(cardf);
			edo.DoSimpleValueWriteToLocation(BAPLayoutEntry.INVALID_ARRAY_INDEX, cardp, pcard, time, line);

			ENumeric pcap = new ENumeric((IRSignedIntegerType)cardf.FieldType, INIT_CAPACITY);
			IRBasicAccessPath capp = ExeProgram.TProg.GetAccessPathForSingleField(capf);
			edo.DoSimpleValueWriteToLocation(BAPLayoutEntry.INVALID_ARRAY_INDEX, capp, pcap, time, line);

			return edo;
		}

		public override string ToString()
		{
			StringBuilder sb = new StringBuilder("[" + this.m_loctype.ToString() + ": ");
			sb.Append(this.m_fieldinfo.ToString());
			sb.Append("]");

			return sb.ToString();
		}
	}
}
